0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 7591 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 66 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 249 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 17 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPSizeChangeProof (⇔, 0 ms)
↳43 YES
↳44 PiDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 PiDP
↳47 PiDPToQDPProof (⇒, 0 ms)
↳48 QDP
↳49 QDPSizeChangeProof (⇔, 0 ms)
↳50 YES
↳51 PiDP
↳52 UsableRulesProof (⇔, 0 ms)
↳53 PiDP
↳54 PiDPToQDPProof (⇒, 0 ms)
↳55 QDP
↳56 QDPSizeChangeProof (⇔, 0 ms)
↳57 YES
↳58 PiDP
↳59 UsableRulesProof (⇔, 0 ms)
↳60 PiDP
↳61 PiDPToQDPProof (⇒, 0 ms)
↳62 QDP
↳63 QDPSizeChangeProof (⇔, 0 ms)
↳64 YES
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotH_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTH_IN_GGA(T7, T8, T10)
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → U8_GGA(T77, T79, quotA_in_ga(T77, T79))
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → QUOTA_IN_GA(T77, T79)
QUOTA_IN_GA(s(T106), s(T108)) → U1_GA(T106, T108, quotA_in_ga(T106, T108))
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U9_GGA(T183, T185, quotB_in_ga(T183, T185))
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTB_IN_GA(T183, T185)
QUOTB_IN_GA(s(s(T230)), s(T232)) → U2_GA(T230, T232, quotB_in_ga(T230, T232))
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_GGA(T307, T309, quotC_in_ga(T307, T309))
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTC_IN_GA(T307, T309)
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → U3_GA(T372, T374, quotC_in_ga(T372, T374))
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_GGA(T449, T451, quotD_in_ga(T449, T451))
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTD_IN_GA(T449, T451)
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → U4_GA(T532, T534, quotD_in_ga(T532, T534))
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_GGA(T609, T611, quotE_in_ga(T609, T611))
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTE_IN_GA(T609, T611)
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U5_GA(T710, T712, quotE_in_ga(T710, T712))
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_GGA(T787, T789, quotF_in_ga(T787, T789))
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTF_IN_GA(T787, T789)
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U6_GA(T906, T908, quotF_in_ga(T906, T908))
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_GGA(T983, T985, quotG_in_ga(T983, T985))
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTG_IN_GA(T983, T985)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_GA(T1120, T1122, quotG_in_ga(T1120, T1122))
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_GGA(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → U16_GGGA(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U17_GGGA(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
DIVJ_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quotH_in_gga(T7, T8, T10))
DIVJ_IN_GGA(T7, T8, T10) → QUOTH_IN_GGA(T7, T8, T10)
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → U8_GGA(T77, T79, quotA_in_ga(T77, T79))
QUOTH_IN_GGA(s(T77), s(0), s(T79)) → QUOTA_IN_GA(T77, T79)
QUOTA_IN_GA(s(T106), s(T108)) → U1_GA(T106, T108, quotA_in_ga(T106, T108))
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → U9_GGA(T183, T185, quotB_in_ga(T183, T185))
QUOTH_IN_GGA(s(s(T183)), s(s(0)), s(T185)) → QUOTB_IN_GA(T183, T185)
QUOTB_IN_GA(s(s(T230)), s(T232)) → U2_GA(T230, T232, quotB_in_ga(T230, T232))
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_GGA(T307, T309, quotC_in_ga(T307, T309))
QUOTH_IN_GGA(s(s(s(T307))), s(s(s(0))), s(T309)) → QUOTC_IN_GA(T307, T309)
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → U3_GA(T372, T374, quotC_in_ga(T372, T374))
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_GGA(T449, T451, quotD_in_ga(T449, T451))
QUOTH_IN_GGA(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → QUOTD_IN_GA(T449, T451)
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → U4_GA(T532, T534, quotD_in_ga(T532, T534))
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_GGA(T609, T611, quotE_in_ga(T609, T611))
QUOTH_IN_GGA(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → QUOTE_IN_GA(T609, T611)
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → U5_GA(T710, T712, quotE_in_ga(T710, T712))
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_GGA(T787, T789, quotF_in_ga(T787, T789))
QUOTH_IN_GGA(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → QUOTF_IN_GA(T787, T789)
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → U6_GA(T906, T908, quotF_in_ga(T906, T908))
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_GGA(T983, T985, quotG_in_ga(T983, T985))
QUOTH_IN_GGA(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → QUOTG_IN_GA(T983, T985)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_GA(T1120, T1122, quotG_in_ga(T1120, T1122))
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_GGA(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → U16_GGGA(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → U17_GGGA(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → QUOTG_IN_GA(T1120, T1122)
QUOTG_IN_GA(s(s(s(s(s(s(s(T1120)))))))) → QUOTG_IN_GA(T1120)
From the DPs we obtained the following set of size-change graphs:
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTF_IN_GA(s(s(s(s(s(s(T906)))))), s(T908)) → QUOTF_IN_GA(T906, T908)
QUOTF_IN_GA(s(s(s(s(s(s(T906))))))) → QUOTF_IN_GA(T906)
From the DPs we obtained the following set of size-change graphs:
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTE_IN_GA(s(s(s(s(s(T710))))), s(T712)) → QUOTE_IN_GA(T710, T712)
QUOTE_IN_GA(s(s(s(s(s(T710)))))) → QUOTE_IN_GA(T710)
From the DPs we obtained the following set of size-change graphs:
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTD_IN_GA(s(s(s(s(T532)))), s(T534)) → QUOTD_IN_GA(T532, T534)
QUOTD_IN_GA(s(s(s(s(T532))))) → QUOTD_IN_GA(T532)
From the DPs we obtained the following set of size-change graphs:
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTC_IN_GA(s(s(s(T372))), s(T374)) → QUOTC_IN_GA(T372, T374)
QUOTC_IN_GA(s(s(s(T372)))) → QUOTC_IN_GA(T372)
From the DPs we obtained the following set of size-change graphs:
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTB_IN_GA(s(s(T230)), s(T232)) → QUOTB_IN_GA(T230, T232)
QUOTB_IN_GA(s(s(T230))) → QUOTB_IN_GA(T230)
From the DPs we obtained the following set of size-change graphs:
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTA_IN_GA(s(T106), s(T108)) → QUOTA_IN_GA(T106, T108)
QUOTA_IN_GA(s(T106)) → QUOTA_IN_GA(T106)
From the DPs we obtained the following set of size-change graphs:
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)
divJ_in_gga(T7, T8, T10) → U18_gga(T7, T8, T10, quotH_in_gga(T7, T8, T10))
quotH_in_gga(0, s(T15), 0) → quotH_out_gga(0, s(T15), 0)
quotH_in_gga(s(0), s(s(T68)), 0) → quotH_out_gga(s(0), s(s(T68)), 0)
quotH_in_gga(s(T77), s(0), s(T79)) → U8_gga(T77, T79, quotA_in_ga(T77, T79))
quotA_in_ga(0, 0) → quotA_out_ga(0, 0)
quotA_in_ga(s(T106), s(T108)) → U1_ga(T106, T108, quotA_in_ga(T106, T108))
U1_ga(T106, T108, quotA_out_ga(T106, T108)) → quotA_out_ga(s(T106), s(T108))
U8_gga(T77, T79, quotA_out_ga(T77, T79)) → quotH_out_gga(s(T77), s(0), s(T79))
quotH_in_gga(s(s(0)), s(s(s(T174))), 0) → quotH_out_gga(s(s(0)), s(s(s(T174))), 0)
quotH_in_gga(s(s(T183)), s(s(0)), s(T185)) → U9_gga(T183, T185, quotB_in_ga(T183, T185))
quotB_in_ga(0, 0) → quotB_out_ga(0, 0)
quotB_in_ga(s(0), 0) → quotB_out_ga(s(0), 0)
quotB_in_ga(s(s(T230)), s(T232)) → U2_ga(T230, T232, quotB_in_ga(T230, T232))
U2_ga(T230, T232, quotB_out_ga(T230, T232)) → quotB_out_ga(s(s(T230)), s(T232))
U9_gga(T183, T185, quotB_out_ga(T183, T185)) → quotH_out_gga(s(s(T183)), s(s(0)), s(T185))
quotH_in_gga(s(s(s(0))), s(s(s(s(T298)))), 0) → quotH_out_gga(s(s(s(0))), s(s(s(s(T298)))), 0)
quotH_in_gga(s(s(s(T307))), s(s(s(0))), s(T309)) → U10_gga(T307, T309, quotC_in_ga(T307, T309))
quotC_in_ga(0, 0) → quotC_out_ga(0, 0)
quotC_in_ga(s(0), 0) → quotC_out_ga(s(0), 0)
quotC_in_ga(s(s(0)), 0) → quotC_out_ga(s(s(0)), 0)
quotC_in_ga(s(s(s(T372))), s(T374)) → U3_ga(T372, T374, quotC_in_ga(T372, T374))
U3_ga(T372, T374, quotC_out_ga(T372, T374)) → quotC_out_ga(s(s(s(T372))), s(T374))
U10_gga(T307, T309, quotC_out_ga(T307, T309)) → quotH_out_gga(s(s(s(T307))), s(s(s(0))), s(T309))
quotH_in_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0) → quotH_out_gga(s(s(s(s(0)))), s(s(s(s(s(T440))))), 0)
quotH_in_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451)) → U11_gga(T449, T451, quotD_in_ga(T449, T451))
quotD_in_ga(0, 0) → quotD_out_ga(0, 0)
quotD_in_ga(s(0), 0) → quotD_out_ga(s(0), 0)
quotD_in_ga(s(s(0)), 0) → quotD_out_ga(s(s(0)), 0)
quotD_in_ga(s(s(s(0))), 0) → quotD_out_ga(s(s(s(0))), 0)
quotD_in_ga(s(s(s(s(T532)))), s(T534)) → U4_ga(T532, T534, quotD_in_ga(T532, T534))
U4_ga(T532, T534, quotD_out_ga(T532, T534)) → quotD_out_ga(s(s(s(s(T532)))), s(T534))
U11_gga(T449, T451, quotD_out_ga(T449, T451)) → quotH_out_gga(s(s(s(s(T449)))), s(s(s(s(0)))), s(T451))
quotH_in_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0) → quotH_out_gga(s(s(s(s(s(0))))), s(s(s(s(s(s(T600)))))), 0)
quotH_in_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611)) → U12_gga(T609, T611, quotE_in_ga(T609, T611))
quotE_in_ga(0, 0) → quotE_out_ga(0, 0)
quotE_in_ga(s(0), 0) → quotE_out_ga(s(0), 0)
quotE_in_ga(s(s(0)), 0) → quotE_out_ga(s(s(0)), 0)
quotE_in_ga(s(s(s(0))), 0) → quotE_out_ga(s(s(s(0))), 0)
quotE_in_ga(s(s(s(s(0)))), 0) → quotE_out_ga(s(s(s(s(0)))), 0)
quotE_in_ga(s(s(s(s(s(T710))))), s(T712)) → U5_ga(T710, T712, quotE_in_ga(T710, T712))
U5_ga(T710, T712, quotE_out_ga(T710, T712)) → quotE_out_ga(s(s(s(s(s(T710))))), s(T712))
U12_gga(T609, T611, quotE_out_ga(T609, T611)) → quotH_out_gga(s(s(s(s(s(T609))))), s(s(s(s(s(0))))), s(T611))
quotH_in_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0) → quotH_out_gga(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T778))))))), 0)
quotH_in_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789)) → U13_gga(T787, T789, quotF_in_ga(T787, T789))
quotF_in_ga(0, 0) → quotF_out_ga(0, 0)
quotF_in_ga(s(0), 0) → quotF_out_ga(s(0), 0)
quotF_in_ga(s(s(0)), 0) → quotF_out_ga(s(s(0)), 0)
quotF_in_ga(s(s(s(0))), 0) → quotF_out_ga(s(s(s(0))), 0)
quotF_in_ga(s(s(s(s(0)))), 0) → quotF_out_ga(s(s(s(s(0)))), 0)
quotF_in_ga(s(s(s(s(s(0))))), 0) → quotF_out_ga(s(s(s(s(s(0))))), 0)
quotF_in_ga(s(s(s(s(s(s(T906)))))), s(T908)) → U6_ga(T906, T908, quotF_in_ga(T906, T908))
U6_ga(T906, T908, quotF_out_ga(T906, T908)) → quotF_out_ga(s(s(s(s(s(s(T906)))))), s(T908))
U13_gga(T787, T789, quotF_out_ga(T787, T789)) → quotH_out_gga(s(s(s(s(s(s(T787)))))), s(s(s(s(s(s(0)))))), s(T789))
quotH_in_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0) → quotH_out_gga(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T974)))))))), 0)
quotH_in_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985)) → U14_gga(T983, T985, quotG_in_ga(T983, T985))
quotG_in_ga(0, 0) → quotG_out_ga(0, 0)
quotG_in_ga(s(0), 0) → quotG_out_ga(s(0), 0)
quotG_in_ga(s(s(0)), 0) → quotG_out_ga(s(s(0)), 0)
quotG_in_ga(s(s(s(0))), 0) → quotG_out_ga(s(s(s(0))), 0)
quotG_in_ga(s(s(s(s(0)))), 0) → quotG_out_ga(s(s(s(s(0)))), 0)
quotG_in_ga(s(s(s(s(s(0))))), 0) → quotG_out_ga(s(s(s(s(s(0))))), 0)
quotG_in_ga(s(s(s(s(s(s(0)))))), 0) → quotG_out_ga(s(s(s(s(s(s(0)))))), 0)
quotG_in_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122)) → U7_ga(T1120, T1122, quotG_in_ga(T1120, T1122))
U7_ga(T1120, T1122, quotG_out_ga(T1120, T1122)) → quotG_out_ga(s(s(s(s(s(s(s(T1120))))))), s(T1122))
U14_gga(T983, T985, quotG_out_ga(T983, T985)) → quotH_out_gga(s(s(s(s(s(s(s(T983))))))), s(s(s(s(s(s(s(0))))))), s(T985))
quotH_in_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → U15_gga(T1176, T1181, T1149, quotI_in_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149))
quotI_in_ggga(0, s(T1197), T1198, 0) → quotI_out_ggga(0, s(T1197), T1198, 0)
quotI_in_ggga(T1211, 0, T1212, s(T1214)) → U16_ggga(T1211, T1212, T1214, quotH_in_gga(T1211, s(T1212), T1214))
U16_ggga(T1211, T1212, T1214, quotH_out_gga(T1211, s(T1212), T1214)) → quotI_out_ggga(T1211, 0, T1212, s(T1214))
quotI_in_ggga(s(T1261), s(T1266), T1230, T1232) → U17_ggga(T1261, T1266, T1230, T1232, quotI_in_ggga(T1261, T1266, T1230, T1232))
U17_ggga(T1261, T1266, T1230, T1232, quotI_out_ggga(T1261, T1266, T1230, T1232)) → quotI_out_ggga(s(T1261), s(T1266), T1230, T1232)
U15_gga(T1176, T1181, T1149, quotI_out_ggga(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)) → quotH_out_gga(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149)
U18_gga(T7, T8, T10, quotH_out_gga(T7, T8, T10)) → divJ_out_gga(T7, T8, T10)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181)))))))), T1149) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))), T1149)
QUOTI_IN_GGGA(T1211, 0, T1212, s(T1214)) → QUOTH_IN_GGA(T1211, s(T1212), T1214)
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230, T1232) → QUOTI_IN_GGGA(T1261, T1266, T1230, T1232)
QUOTH_IN_GGA(s(s(s(s(s(s(s(s(T1176)))))))), s(s(s(s(s(s(s(s(T1181))))))))) → QUOTI_IN_GGGA(T1176, T1181, s(s(s(s(s(s(s(T1181))))))))
QUOTI_IN_GGGA(T1211, 0, T1212) → QUOTH_IN_GGA(T1211, s(T1212))
QUOTI_IN_GGGA(s(T1261), s(T1266), T1230) → QUOTI_IN_GGGA(T1261, T1266, T1230)
From the DPs we obtained the following set of size-change graphs: